Nuprl Lemma : fpf-disjoint-compatible
11,40
postcript
pdf
A
:Type,
eq
:EqDecider(
A
),
B
:(
A
Type),
f
,
g
:
a
:
A
fp
B
(
a
). l_disjoint(
A
;
f
.1;
g
.1)
f
||
g
latex
Definitions
b
,
t
T
,
x
:
A
.
B
(
x
)
,
EqDecider(
T
)
,
x
(
s
)
,
(
x
l
)
,
x
.
t
(
x
)
,
t
.1
,
l_disjoint(
T
;
l1
;
l2
)
,
deq-member(
eq
;
x
;
L
)
,
,
P
&
Q
,
t
.2
,
P
Q
,
f
(
x
)
,
x
dom(
f
)
,
f
||
g
,
a
:
A
fp
B
(
a
)
,
False
,
A
,
P
Q
Lemmas
assert-deq-member
,
assert
wf
,
deq-member
wf
,
l
disjoint
wf
,
pi1
wf
,
l
member
wf
,
deq
wf
origin
A:Type, eq:EqDecider(A), B:(A
Type), f, g:a:A fp B(a). l_disjoint(A;f.1;g.1) 
f || g A:Type, eq:EqDecider(A), B:(AType), f, g:a:A fp B(a). l_disjoint(A;f.1;g.1) f || g 
b
Tx:A. B(x) l)
x. t(x)
Q dom(f) B(a)
A
Q